#!/usr/bin/python
# encoding: utf-8
# 所有利用不等式证明的问题
from mathsolver.functions.budengshi import common_opers as co
from mathsolver.functions.mathematica.mathematicaSolve import *
from itertools import combinations
from functools import reduce


# 不等式 证明， 用到 分析法， 间接法， 综合法
class ZhengMing001(BaseFunction):
    def solver(self, *args):
        cond_ineqs = None
        if len(args) == 2:
            if isinstance(args[0], BaseBelong):
                if args[0].interval == 'R':
                    cond_ineqs = map(lambda v: (v, S.Reals), args[0].var)
            else:
                cond_ineqs = args[0].ineqs
        prove_ineq = args[-1]
        left, op, right = prove_ineq.sympify()
        f = left - right
        if cond_ineqs:
            ineqs_print = ''
            for ineq in cond_ineqs:
                if co.iterable(ineq) and len(ineq) == 2:
                    ineq = list(ineq)
                    ineqs_print += '%s \\in %s' % (new_latex(ineq[0]), new_latex(ineq[1]))
                elif len(ineq.value) == 2 and str(ineq.value[0]) == '0':
                    ineqs_print += ', ' + ''.join(ineq.value[1])
                else:
                    ineqs_print += ', ' + ineq.printing()
            self.steps.append([r'\because ', ineqs_print])
            self.steps.append([r'%s ' % prove_ineq.printing(), ' => ' + new_latex(f) + op + '0'])
            self.steps.append([r'\because %s =' % new_latex(f), ' = ' + new_latex(factor(expand(f))) + op + '0'])
        else:
            self.steps.append([r'\therefore %s ' % prove_ineq.printing(), ' => ' + new_latex(f) + op + '0'])
            self.steps.append([r'\because %s =' % new_latex(f), ' = ' + new_latex(factor(expand(f))) + op + '0'])
        self.label.add('不等式证明')
        return self


class ZhengMing002(BaseFunction):
    """
    求证:\\sqrt{3}+\\sqrt{7}<2\\sqrt{5}.
    """
    def solver(self, *args):
        ineq = args[0]
        l, op, r = ineq.sympify()
        self.label.add('不等式证明')
        if l.is_real and r.is_real:
            l_square = expand(l ** 2)
            r_square = expand(r ** 2)
            self.steps.append(['\because %s 和 %s' % (new_latex(l), new_latex(r)), '都是实数'])
            self.steps.append(['若证 ' + ineq.printing(), ''])
            self.steps.append(['只需证 %s %s %s' % (new_latex(l ** 2), op, new_latex(r ** 2)), ''])
            self.steps.append(['\because %s %s %s 当然成立' % (new_latex(l_square), op, new_latex(r_square)), ''])
            self.steps.append(['\therefore 原不等式成立', ''])
            return self
        else:
            raise Exception('try error')


# paramer1 Func; paramer2 Expression; paramer3 Ineq
class ZhengMing003(BaseFunction):
    """
    设函数f(x)=|x+\\frac{1}{a}|+|x-a|(a>0).证明:f(x)≥2
    """
    def solver(self, *args):
        self.label.add('不等式证明')
        arg0 = args[0]
        arg1 = args[1]
        ineq = args[2]
        op = 'Minimize' if arg1.value.find('>') >= 0 else 'Maximize'
        min_value = MathematicaOptimize().solver(BaseOptimize(arg0.expression, op, ineq), None).output[0].sympify()
        self.steps.append(['\\therefore f(x)的最小值为', new_latex(min_value)])
        return self


# paramer1 eq; paramer2 ineq
class ZhengMing004(BaseFunction):
    """
    1. 设a,b,c均为正数,a+b+c=1,证明: ab+bc+ca≤\\frac{1}{3}
    2. 设a,b,c均为正数,a+b+c=1,证明: \\frac{{a}^{2}}{b}+\\frac{{b}^{2}}{c}+\\frac{{c}^{2}}{a}≥1
    """
    def solver(self, *args):
        self.label.add('不等式证明')
        eq = args[0]
        ineq = args[1]
        eq_l, eq_r = eq.sympify()
        eq_l_squad_expand = expand(eq_l ** 2)
        eq_f = eq_l - eq_r
        symbs = sorted(list(eq_f.free_symbols), key=str)
        if len(symbs) != 3:
            raise Exception('Type Match Error')
        ineq_l, _, ineq_r = ineq.sympify()
        if not ineq_r.is_real:
            raise Exception('Type Match Error')
        symb_combins = list(combinations(symbs, 2))
        combin_ineqs = list(map(lambda _: BaseIneq([_[0] ** 2 + _[1] ** 2, '>=', 2 * _[0] * _[1]]), symb_combins))
        self.steps.append(['由' + combin_ineqs[0].printing() + ',' + combin_ineqs[1].printing() + ',' + combin_ineqs[2].printing(), '得：'])
        f1 = reduce(lambda _1, _2: _1 + _2, list(map(lambda s: s ** 2, symbs)))
        f2 = reduce(lambda _1, _2: _1 + _2, list(map(lambda _: _[0] * _[1], symb_combins)))
        self.steps.append([BaseIneq([f1, '>=', f2]).printing(), ''])
        self.steps.append(['由题设得:' + BaseEq([eq_l ** 2, eq_r ** 2]).printing(),
                           '即，' + BaseEq([eq_l_squad_expand, eq_r ** 2]).printing()])
        f1_sub = solve(eq_l_squad_expand - eq_r ** 2, f1)[0]
        self.steps.append(['即' + new_latex(f1) + '=' + new_latex(f1_sub), ';' + BaseIneq([f1_sub, '>=', f2]).printing()])
        self.steps.append(['所以', ineq.printing()])
        return self


# 证明的元函数
class ZhengMing(BaseFunction):
    CLS = [ZhengMing003, ZhengMing001, ZhengMing002, ZhengMing004]

    def solver(self, *args):
        r = None
        for cl in ZhengMing.CLS:
            try:
                r = cl(verbose=True)
                r.known = self.known
                r = r.solver(*args)
                break
            except Exception:
                r = None
        if None:
            raise 'try fail'
        return r


if __name__ == '__main__':
    pass
